(declare-fun n3 () Int)
(declare-fun n5 () Int)
(declare-fun n7 () Int)
(declare-fun n9 () Int)
(declare-fun n10 () Int)
(declare-fun n13 () Int)
(declare-fun n15 () Int)
(assert (> n3 1))
(assert (>= n7 1))
(assert (= n10 n3))
(declare-fun n16 () Int)
(assert (= n16 (* n7 n7)))
(declare-fun n19 () Int)
(assert (= n19 (* n13 n13)))
(declare-fun n21 () Int)
(declare-fun n22 () Int)
(assert (= 1 (* n7 n19)))
(assert (= 0 (* n5 n21)))
(declare-fun n27 () Int)
(declare-fun n29 () Int)
(assert (= n29 (* n3 n15)))
(declare-fun n30 () Int)
(assert (= n30 (+ n9 n29)))
(declare-fun n31 () Int)
(assert (= n31 (* n3 n16)))
(declare-fun n36 () Int)
(declare-fun n37 () Int)
(assert true)
(declare-fun n38 () Int)
(assert (= n38 (* n31 n9)))
(declare-fun n39 () Int)
(assert (= n39 (+ n9 n38)))
(declare-fun n40 () Int)
(assert true)
(declare-fun n41 () Int)
(assert (= n41 (* n37 n9)))
(declare-fun n42 () Int)
(assert (= n42 (+ n36 n41)))
(declare-fun n43 () Int)
(assert (= n43 n7))
(assert (= n39 n42))
(assert (= n40 0))
(declare-fun n44 () Int)
(assert (= n44 1))
(declare-fun n45 () Int)
(assert (= n45 (+ (mod (* n31 n3) (* n19 n15)))))
(assert (> n45 n27))
(declare-fun n47 () Int)
(assert (= n47 (* n19 n15)))
(declare-fun n48 () Int)
(assert (= n48 (+ n36 n47)))
(assert (> n48 n21))
(assert (= 0 (* n43 n27)))
(declare-fun n57 () Int)
(assert (= n57 n30))
(declare-fun n58 () Int)
(assert (= n58 (* n7 n31)))
(assert (> n21 n57))
(assert (= n37 n58))
(check-sat)
